﻿module Coq.MonoDevelop.Scope

open Ast
open Coq.MonoDevelop.Helpers

//ScopeState is Location, list of ids defined in the scope and a list of subscopes
type ScopeState = 
  | ScopeState of list<Identifier> * Location * list<ScopeState>

///////////////////////////////////////Helper Functions///////////////////////////////////////////

let rec GetScopeStateIdentifiers pos (ss:ScopeState) =    
    let (ScopeState(liid, loc, lss)) = ss
    if (Common.IsPartOf pos loc) then
        liid @ Common.Merge (GetScopeStateIdentifiers pos) lss
    else 
        []

//////////////////////////////////////AST Walkers///////////////////////////////////////////////////////
let rec CoqASTWalker ast = 
    match ast with
      | CoqAST(sl,l) ->
            let (s,e) = l
            ScopeState([], l, List.collect (SentenceWalker e) sl)

and SentenceWalker endLoc s = 
    match s with
    | Sentence.Assumption(ak, la, (sp, ep)) -> [ ScopeState(Common.Merge AssumeNameWalker la, (ep, endLoc), []) ]
    | Sentence.Definition (def, (sp, ep)) ->  [ ScopeState(DefinitionNameWalker def, (ep, endLoc), []) ]
    | Sentence.AssertionBlock (ass, p, (sp, ep)) -> 
        match p with 
        | Some(Proof(til,s,(lsp,lep)))  -> [ ScopeState(AssertionNameWalker ass, (lsp, endLoc), []) ]  //List.map (TacticInvocationWalker lep) til -- to do at least remember intro H 
        | _ (*None*) -> [ ScopeState(AssertionNameWalker ass, (ep, endLoc), []) ]
    | _ -> []

and AssumeNameWalker a =
    match a with 
    | Assume (il, t) -> il

and DefinitionNameWalker d = 
    match d with 
    | DefinitionD(id, b, ot, t) -> [ id ]
    | Let (id, b, ot, t) -> [ id ] 

and AssertionNameWalker a = 
    match a with 
    | Assertion(ak, id, ob, t) -> [ id ]

and TacticInvocationWalker endLoc ti = 
    match ti with
    | TacticInvocation(num, t, (sp,ep)) -> ScopeState (TacticNameWalker t, (ep, endLoc), [])

    

and TacticNameWalker t = 
    match t with
    | TacticNoArg(id) -> [ id ]
    | TatcticOneArg(id,t) -> [ id ]


